eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
↳ QTRS
↳ Non-Overlap Check
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
eq2(0, 0)
eq2(0, s1(x0))
eq2(s1(x0), 0)
eq2(s1(x0), s1(x1))
rm2(x0, nil)
rm2(x0, add2(x1, x2))
ifrm3(true, x0, add2(x1, x2))
ifrm3(false, x0, add2(x1, x2))
purge1(nil)
purge1(add2(x0, x1))
PURGE1(add2(N, X)) -> RM2(N, X)
PURGE1(add2(N, X)) -> PURGE1(rm2(N, X))
EQ2(s1(X), s1(Y)) -> EQ2(X, Y)
IFRM3(true, N, add2(M, X)) -> RM2(N, X)
IFRM3(false, N, add2(M, X)) -> RM2(N, X)
RM2(N, add2(M, X)) -> EQ2(N, M)
RM2(N, add2(M, X)) -> IFRM3(eq2(N, M), N, add2(M, X))
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
eq2(0, 0)
eq2(0, s1(x0))
eq2(s1(x0), 0)
eq2(s1(x0), s1(x1))
rm2(x0, nil)
rm2(x0, add2(x1, x2))
ifrm3(true, x0, add2(x1, x2))
ifrm3(false, x0, add2(x1, x2))
purge1(nil)
purge1(add2(x0, x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
PURGE1(add2(N, X)) -> RM2(N, X)
PURGE1(add2(N, X)) -> PURGE1(rm2(N, X))
EQ2(s1(X), s1(Y)) -> EQ2(X, Y)
IFRM3(true, N, add2(M, X)) -> RM2(N, X)
IFRM3(false, N, add2(M, X)) -> RM2(N, X)
RM2(N, add2(M, X)) -> EQ2(N, M)
RM2(N, add2(M, X)) -> IFRM3(eq2(N, M), N, add2(M, X))
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
eq2(0, 0)
eq2(0, s1(x0))
eq2(s1(x0), 0)
eq2(s1(x0), s1(x1))
rm2(x0, nil)
rm2(x0, add2(x1, x2))
ifrm3(true, x0, add2(x1, x2))
ifrm3(false, x0, add2(x1, x2))
purge1(nil)
purge1(add2(x0, x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
EQ2(s1(X), s1(Y)) -> EQ2(X, Y)
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
eq2(0, 0)
eq2(0, s1(x0))
eq2(s1(x0), 0)
eq2(s1(x0), s1(x1))
rm2(x0, nil)
rm2(x0, add2(x1, x2))
ifrm3(true, x0, add2(x1, x2))
ifrm3(false, x0, add2(x1, x2))
purge1(nil)
purge1(add2(x0, x1))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
EQ2(s1(X), s1(Y)) -> EQ2(X, Y)
trivial
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
eq2(0, 0)
eq2(0, s1(x0))
eq2(s1(x0), 0)
eq2(s1(x0), s1(x1))
rm2(x0, nil)
rm2(x0, add2(x1, x2))
ifrm3(true, x0, add2(x1, x2))
ifrm3(false, x0, add2(x1, x2))
purge1(nil)
purge1(add2(x0, x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
IFRM3(true, N, add2(M, X)) -> RM2(N, X)
IFRM3(false, N, add2(M, X)) -> RM2(N, X)
RM2(N, add2(M, X)) -> IFRM3(eq2(N, M), N, add2(M, X))
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
eq2(0, 0)
eq2(0, s1(x0))
eq2(s1(x0), 0)
eq2(s1(x0), s1(x1))
rm2(x0, nil)
rm2(x0, add2(x1, x2))
ifrm3(true, x0, add2(x1, x2))
ifrm3(false, x0, add2(x1, x2))
purge1(nil)
purge1(add2(x0, x1))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
IFRM3(true, N, add2(M, X)) -> RM2(N, X)
IFRM3(false, N, add2(M, X)) -> RM2(N, X)
Used ordering: Combined order from the following AFS and order.
RM2(N, add2(M, X)) -> IFRM3(eq2(N, M), N, add2(M, X))
[true, 0] > false
s1 > false
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
RM2(N, add2(M, X)) -> IFRM3(eq2(N, M), N, add2(M, X))
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
eq2(0, 0)
eq2(0, s1(x0))
eq2(s1(x0), 0)
eq2(s1(x0), s1(x1))
rm2(x0, nil)
rm2(x0, add2(x1, x2))
ifrm3(true, x0, add2(x1, x2))
ifrm3(false, x0, add2(x1, x2))
purge1(nil)
purge1(add2(x0, x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
PURGE1(add2(N, X)) -> PURGE1(rm2(N, X))
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
eq2(0, 0)
eq2(0, s1(x0))
eq2(s1(x0), 0)
eq2(s1(x0), s1(x1))
rm2(x0, nil)
rm2(x0, add2(x1, x2))
ifrm3(true, x0, add2(x1, x2))
ifrm3(false, x0, add2(x1, x2))
purge1(nil)
purge1(add2(x0, x1))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
PURGE1(add2(N, X)) -> PURGE1(rm2(N, X))
add1 > PURGE1 > false
nil > false
0 > true > false
rm2(N, nil) -> nil
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
eq2(0, 0) -> true
eq2(0, s1(X)) -> false
eq2(s1(X), 0) -> false
eq2(s1(X), s1(Y)) -> eq2(X, Y)
rm2(N, nil) -> nil
rm2(N, add2(M, X)) -> ifrm3(eq2(N, M), N, add2(M, X))
ifrm3(true, N, add2(M, X)) -> rm2(N, X)
ifrm3(false, N, add2(M, X)) -> add2(M, rm2(N, X))
purge1(nil) -> nil
purge1(add2(N, X)) -> add2(N, purge1(rm2(N, X)))
eq2(0, 0)
eq2(0, s1(x0))
eq2(s1(x0), 0)
eq2(s1(x0), s1(x1))
rm2(x0, nil)
rm2(x0, add2(x1, x2))
ifrm3(true, x0, add2(x1, x2))
ifrm3(false, x0, add2(x1, x2))
purge1(nil)
purge1(add2(x0, x1))